natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
What is called observational type theory (OTT) is a flavor of type theory in between extensional type theory and intensional type theory.
This may be regarded as a first-stage approximation to homotopy type theory (HoTT, and for more motivation see at higher observational type theory):
The propositions of OTT correspond to the h-propositions of HoTT, and the types in OTT correspond to h-sets in HoTT. The notion of equality on OTT is based on symmetric prosets, which is a special case of higher internal groupoids. Since equality is defined type-by-type, OTT enjoys function extensionality, and a form of propositional extensionality at least for a specified universe of propositions (not necessarily including all h-propositions).
There are a few technical differences (e.g. proofs of propositions are definitionally equal in OTT, whereas proofs of hprops are only propositionally equal in HoTT) but on the whole HoTT looks a lot like a higher homotopy version of OTT.
Observational type theory was introduced in:
Thorsten Altenkirch, Conor McBride, Towards observational type theory, draft (2006) [pdf, pdf, pdf]
Thorsten Altenkirch, Conor McBride, Wouter Swierstra, Observational Equality, Now!, PLPV ‘07: Proceedings of the 2007 workshop on Programming languages meets program verification (2007) 57-68 [ISBN:978-1-59593-677-6, doi:10.1145/1292597.1292608, pdf]
A blog post about an Agda implementation, including propositional extensionality (which is not mentioned in ABS07):
The above comparison between OTT and HoTT is taken from
Metatheoretical properties of OTT are proved in
Loïc Pujet, Nicolas Tabareau, Observational Equality: Now for Good, POPL’22, pdf
Loïc Pujet, Nicolas Tabareau, Impredicative Observational Equality, POPL’23, pdf
Loïc Pujet, Nicolas Tabareau, Observational Equality Meets CIC, ESOP’24, pdf
Last revised on August 19, 2024 at 12:48:09. See the history of this page for a list of all contributions to it.